Nuprl Definition : ma-join 0,22

M1  M2
== mk-ma(1of(M1 1of(M2);
== 1of(2of(M1))  1of(2of(M2));
== 1of(2of(2of(M1)))  1of(2of(2of(M2)));
== 1of(2of(2of(2of(M1))))  1of(2of(2of(2of(M2))));
== 1of(2of(2of(2of(2of(M1)))))  1of(2of(2of(2of(2of(M2)))));
== 1of(2of(2of(2of(2of(2of(M1))))))  1of(2of(2of(2of(2of(2of(M2))))));
== 1of(2of(2of(2of(2of(2of(2of(M1)))))))  1of(2of(2of(2of(2of(2of(2of(M2)))))));
== 1of(2of(2of(2of(2of(2of(2of(2of(M1))))))))  1of(2of(2of(2of(2of(2of(2of(2of(M2))))))));
== 1of(2of(2of(2of(2of(2of(2of(2of(2of(M1)))))))))  
== 1of(2of(2of(2of(2of(2of(2of(2of(2of(M2)))))))));
== 1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(M1))))))))))  
== 1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(M2))))))))));
== 1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(M1)))))))))))  
== 1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(M2)))))))))))) 
latex



clarification:

M1  M2
== mk-ma(fpf-join(IdDeq;1of(M1);1of(M2));
== fpf-join(KindDeq;1of(2of(M1));1of(2of(M2)));
== fpf-join(IdDeq;1of(2of(2of(M1)));1of(2of(2of(M2))));
== fpf-join(IdDeq;1of(2of(2of(2of(M1))));1of(2of(2of(2of(M2)))));
== fpf-join(product-deq(Knd;Id;KindDeq;IdDeq);1of(2of(2of(2of(2of(M1)))));1of(2of(2of(2of(2of(
== fpf-join(product-deq(Knd;Id;KindDeq;IdDeq);1of(2of(2of(2of(2of(M1)))));1of(M2))))));
== fpf-join(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);1of(2of(2of(2of(2of(2of(
== fpf-join(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);1of(M1))))));1of(2of(2of(2of(2of(2of(M2)))))));
== fpf-join(IdDeq;1of(2of(2of(2of(2of(2of(2of(M1)))))));1of(2of(2of(2of(2of(2of(2of(M2))))))));
== fpf-join(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);1of(2of(2of(2of(2of(2of(2of(2of(
== fpf-join(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);1of(M1))))))));1of(2of(2of(2of(2of(2of(2of(2of(
== fpf-join(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);1of(M1))))))));1of(M2)))))))));
== fpf-join(KindDeq;1of(2of(2of(2of(2of(2of(2of(2of(2of(
== fpf-join(KindDeq;1of(M1)))))))));1of(2of(2of(2of(2of(2of(2of(2of(2of(M2))))))))));
== fpf-join(KindDeq;1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(
== fpf-join(KindDeq;1of(M1))))))))));1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(M2)))))))))));
== fpf-join(IdDeq;1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(
== fpf-join(IdDeq;1of(M1)))))))))));1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(
== fpf-join(IdDeq;1of(M1)))))))))));1of(M2))))))))))))) 
latex


Definitionsmk-ma, Knd, product-deq(A;B;a;b), IdLnk, Id, IdLnkDeq, KindDeq, f  g, IdDeq, 1of(t), 2of(t)
FDL editor aliasesma-join

origin